(0) Obligation:
Clauses:
even(0) :- !.
even(N) :- ','(p(N, P), odd(P)).
odd(s(0)) :- !.
odd(s(N)) :- even(P).
p(0, 0).
p(s(X), X).
Query: even(g)
(1) PrologToPrologProblemTransformerProof (SOUND transformation)
Built Prolog problem from termination graph ICLP10.
(2) Obligation:
Clauses:
evenA(0).
evenA(s(s(0))).
evenA(s(s(T9))).
Query: evenA(g)
(3) PrologToPiTRSProof (SOUND transformation)
We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
Transforming
Prolog into the following
Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
evenA_in_g(0) → evenA_out_g(0)
evenA_in_g(s(s(0))) → evenA_out_g(s(s(0)))
evenA_in_g(s(s(T9))) → evenA_out_g(s(s(T9)))
The argument filtering Pi contains the following mapping:
evenA_in_g(
x1) =
evenA_in_g(
x1)
0 =
0
evenA_out_g(
x1) =
evenA_out_g
s(
x1) =
s(
x1)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(4) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
evenA_in_g(0) → evenA_out_g(0)
evenA_in_g(s(s(0))) → evenA_out_g(s(s(0)))
evenA_in_g(s(s(T9))) → evenA_out_g(s(s(T9)))
The argument filtering Pi contains the following mapping:
evenA_in_g(
x1) =
evenA_in_g(
x1)
0 =
0
evenA_out_g(
x1) =
evenA_out_g
s(
x1) =
s(
x1)
(5) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
P is empty.
The TRS R consists of the following rules:
evenA_in_g(0) → evenA_out_g(0)
evenA_in_g(s(s(0))) → evenA_out_g(s(s(0)))
evenA_in_g(s(s(T9))) → evenA_out_g(s(s(T9)))
The argument filtering Pi contains the following mapping:
evenA_in_g(
x1) =
evenA_in_g(
x1)
0 =
0
evenA_out_g(
x1) =
evenA_out_g
s(
x1) =
s(
x1)
We have to consider all (P,R,Pi)-chains
(6) Obligation:
Pi DP problem:
P is empty.
The TRS R consists of the following rules:
evenA_in_g(0) → evenA_out_g(0)
evenA_in_g(s(s(0))) → evenA_out_g(s(s(0)))
evenA_in_g(s(s(T9))) → evenA_out_g(s(s(T9)))
The argument filtering Pi contains the following mapping:
evenA_in_g(
x1) =
evenA_in_g(
x1)
0 =
0
evenA_out_g(
x1) =
evenA_out_g
s(
x1) =
s(
x1)
We have to consider all (P,R,Pi)-chains
(7) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,R,Pi) chain.
(8) YES